R-Feasible{i:l}
R-Feasible(Rplus(ecl-machine{ecl:ut2}
R-Feasible(Rplus(ecl-machine(mkid{b:ut2};
R-Feasible(Rplus(ecl-machine(fpf-single(mkid{x:ut2}; );
R-Feasible(Rplus(ecl-machine(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(Kind-deq;
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{a:ut2, b:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{},mkid{x:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single();
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{a:ut2, b:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single(rcv(mklnk{},mkid{y:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-join(fpf-single());
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-single(rcv(mklnk{b:ut2, output:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-single(rcv(mklnk{},mkid{hello:ut2});
R-Feasible(Rplus(ecl-machine(fpf-join(fpf-single());
R-Feasible(Rplus(ecl-machine(eclseq(eclact(eclbase(rcv(mklnk{a:ut2, b:ut2, 1:ut2},mkid{x:ut2});
R-Feasible(Rplus(ecl-machine(eclseq(eclact(eclbase((s,v. (s(mkid{x:ut2})) <z v));
R-Feasible(Rplus(ecl-machine(eclseq(eclact(1);
R-Feasible(Rplus(ecl-machine(eclseq(eclact(eclbase(rcv(mklnk{a:ut2, b:ut2, 1:ut2},mkid{y:ut2});
R-Feasible(Rplus(ecl-machine(eclseq(eclact(eclbase((s,v. v <z (s(mkid{x:ut2}))));
R-Feasible(Rplus(ecl-machine(eclseq(eclact(2));
R-Feasible(Rplus(ecl-machine(msg-spec1(rcv(mklnk{a:ut2, b:ut2, 1:ut2},mkid{y:ut2});
R-Feasible(Rplus(ecl-machine(msg-spec1(mklnk{b:ut2, output:ut2, 1:ut2};
R-Feasible(Rplus(ecl-machine(msg-spec1(mkid{hello:ut2};
R-Feasible(Rplus(ecl-machine(msg-spec1(2;
R-Feasible(Rplus(ecl-machine(msg-spec1(s,v.tt);
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(rcv(mklnk{a:ut2, b:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(rcv(mklnk{},mkid{x:ut2});
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(mkid{x:ut2};
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(1;
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(s,v.v);
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(rcv(mklnk{a:ut2, b:ut2, 1:ut2
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(rcv(mklnk{},mkid{y:ut2});
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(mkid{x:ut2};
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(2;
R-Feasible(Rplus(ecl-machine(update-spec-join(update-spec1(s,v.v)));
R-Feasible(Rplus(Rplus(Rpre(mkid{a:ut2};
R-Feasible(Rplus(Rplus(Rpre(fpf-single(mkid{x:ut2}; );
R-Feasible(Rplus(Rplus(Rpre(mkid{a:ut2};
R-Feasible(Rplus(Rplus(Rpre(unit-fps;
R-Feasible(Rplus(Rplus(Rpre((s.(s(mkid{x:ut2})) <z 10));
R-Feasible(Rplus(Rplus(Rplus(Reffect(mkid{a:ut2};
R-Feasible(Rplus(Rplus(Rplus(Reffect(fpf-single(mkid{x:ut2}; );
R-Feasible(Rplus(Rplus(Rplus(Reffect(locl(mkid{a:ut2});
R-Feasible(Rplus(Rplus(Rplus(Reffect(p-outcome(unit-fps);
R-Feasible(Rplus(Rplus(Rplus(Reffect(mkid{x:ut2};
R-Feasible(Rplus(Rplus(Rplus(Reffect((inl (s,v. (s(mkid{x:ut2})) + 1) ));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{x:ut2}; );
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(locl(mkid{a:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(p-outcome(unit-fps);
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(mklnk{a:ut2, b:ut2, 1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{x:ut2}; );
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends(cons(<mkid{x:ut2}, s,v. cons((s(mkid{x:ut2})); [])>; [])
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rsends();
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-empty;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{input:ut2, a:ut2, 1:ut2},mkid{key:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(mklnk{a:ut2, b:ut2, 1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{y:ut2}; );
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(<mkid{y:ut2}, s,v. cons(v; [])>; []));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-empty;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{input:ut2, a:ut2, 1:ut2
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{},mkid{string:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(atom;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(mklnk{a:ut2, b:ut2, 1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{string:ut2}; atom);
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(<mkid{string:ut2}, s,v. cons(v; [])>; []
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons());
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-empty;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{input:ut2, a:ut2, 1:ut2
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{},mkid{b:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(mklnk{a:ut2, b:ut2, 1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{b:ut2}; );
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(<mkid{b:ut2}, s,v. cons(v; [])>;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons([]));
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-empty;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{input:ut2, a:ut2, 1:ut2
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(rcv(mklnk{},mkid{hello:ut2});
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(Unit;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(mklnk{a:ut2, b:ut2, 1:ut2};
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(fpf-single(mkid{hello:ut2}; Unit);
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(<mkid{hello:ut2}
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(, s,v. cons(v; [])
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons(>;
R-Feasible(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rplus(Rsends(cons([])))))))))) 

latex

Definitions

R-da(R; i), fpf-domain(f), R-has-loc(R; i), decl-type{i:l}(ds; x), Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), outl(x), Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), map(f; as), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), (i = j), lnk-decl(l; dt), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), eq_id(a; b), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), tag(k), eq_lnk(a; b), es realizer ind, source(l), P  Q, P  Q, True, tl(l), i z j, nth_tl(n;as), hd(l), prop{i:l}, guard(T), sq_type(T), l[i], ecl ind, normal-type{i:l}(T), x,y. t(x;y), eq_knd(a; b), b, filter(P; l), ff, fpf-ap(f; eq; x), t.2, eq_atom{$n:n}(x; y), atom2-deq, idlnk-deq, band(p; q), proddeq(a; b), product-deq(A; B; a; b), sumdeq(a; b), union-deq(A; B; a; b), bor(p; q), append(as; bs), t.1, Y, reduce(f; k; as), deq-member(eq; x; L), eqof(d), if b then t else f fi , fpf-cap(f; eq; x; z), ma-valtype(da; k), IdLnk, x. t(x), id-deq, A, fpf-dom(eq; x; f), destination(l), b, ecl-kinds(x), l_all(L; T; x.P(x)), normal-ds{i:l}(ds), P  Q, Knd, Id, A c B, t  T, top, x:A. B(x), R-compat{i:l}(A; B), P  Q, fpf-empty, Rsends(ds; knd; T; l; dt; g), locl(a), Reffect(loc; ds; knd; T; x; f), Rpre(loc; ds; a; p; P), tt, i <z j, eclbase(k; test), eclact(a; n), eclseq(a; b), mklnk{$a:ut2, $b:ut2, $n:ut2}, rcv(l,tg), Kind-deq, fpf-join(eq; f; g), fpf-single(x; v), mkid{$x:ut2}, Rplus(left; right), R-Feasible{i:l}(R), False, P  Q, decidable(P), ||as||, x:A. B(x), (x  l), x(s1,s2), decl-state(ds), , x(s)

Lemmas

ldst wf, lnk wf, lsrc wf, ma-valtype wf, ecl-disjoint-compatible, Rpre wf, fpf-compatible-self, Reffect wf, fpf-empty-compatible-left, p-outcome wf, locl wf, R-compat-Rplus-sq, R-compat-symmetry, Rplus wf, decl-state wf, decl-type wf, Rsends wf, assert-eq-id, lnk-decls-compatible, fpf-compatible-symmetry, lnk-decl-compatible-single, assert-eq-knd, fpf-compatible-singles, fpf-compatible-join2, lnk-decl wf, fpf-compatible-join, fpf-empty wf, fpf-empty-compatible-right, unit wf, it wf, fpf-all-empty, unit-fps wf, natural number wf p-outcome, false wf, msg-spec-loc-decl-spec1, update-spec1-decl, update-spec1 wf2, update-spec-join-decl, l member wf, length wf1, select wf, isrcv wf, assert wf, true wf, decidable int equal, Knd sq, bool-inhabited, normal-da-single, IdLnk wf, normal-da-join, normal-ds-single, fpf-cap-single1, update-spec1 wf, update-spec-join wf, btrue wf, msg-spec1 wf, fpf-single-dom-sq, top wf, fpf-join-cap-sq, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, lt int wf, eclbase wf, eclact wf, eclseq wf, bool wf, Kind-deq wf, rcv wf, fpf-single wf3, Knd wf, fpf-join wf, Id wf, fpf-single wf, ecl-feasible, R-Feasible-Rplus